package dv.network;

import dv.apkeep.BDDEngine;
import dv.apkeep.DeltaForwardingGraph;
import dv.apkeep.Model;
import dv.apkeep.Verifier;
import jdd.bdd.BDD;

import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;

public class Network {

    private HashMap<String, Device> devices;
    public Model model;

    public Network() {
        this.devices = new HashMap<>();
    }

    public HashMap<String, Device> getDevices() {
        return devices;
    }

    public void setModel(Model model) {
        this.model = model;
    }

    public void addDevice(String name) {
        Device device = new Device(name);
        this.devices.put(name, device);
    }

    public void addLink(String fromd, String fromp, String tod, String top) {
        Device fromdev = this.devices.get(fromd);
        Device todev = this.devices.get(tod);
        Port frompt = fromdev.getPortByName(fromp);
        Port topt = todev.getPortByName(top);
        if (frompt == null) {
            frompt = fromdev.addPortByName(fromp);
        }
        if (topt == null) {
            topt = todev.addPortByName(top);
        }
        frompt.setPeer(topt);
        topt.setPeer(frompt);
    }

    public HashSet<Integer> addRule(Device device, Rule rule) {
        HashSet<Change> changes = this.identifyChangesInsert(device, rule);
        return this.model.update(changes);
    }

    private HashSet<Change> identifyChangesInsert(Device device, Rule rule) {
        HashSet<Change> changes = new HashSet<>();
        BDD bdd = this.model.bddEngine.bdd;
        // entrybdd already referred
        int entrybdd = this.model.bddEngine.encodeDstIPPrefix(rule.getKey(), rule.getPrefixLen());
        rule.setMatch(entrybdd);
        rule.setHit(entrybdd);
        boolean bddused = false;
        for (Rule r : device.getRules()) {
            int tmp = bdd.and(r.getHit(), rule.getHit());
            bdd.ref(tmp);
            if (r.getPrefixLen() > rule.getPrefixLen() && tmp != BDDEngine.BDDFalse) {
                int tmp1 = bdd.ref(bdd.not(r.getHit()));
                int tmp2 = bdd.ref(bdd.and(rule.getHit(), tmp1));
                bdd.deref(tmp1);
                bdd.deref(rule.getHit());
                rule.setHit(tmp2);
            }

            if (r.getPrefixLen() < rule.getPrefixLen() && tmp != BDDEngine.BDDFalse) {
                if (r.getOutPort() != rule.getOutPort()) {
                    changes.add(new Change(tmp, r.getOutPort(), rule.getOutPort()));
                    // this bdd is used for handling changes, should not deref
                    bddused = true;
                }

                int tmp1 = bdd.ref(bdd.not(rule.getHit()));
                int tmp2 = bdd.ref(bdd.and(r.getHit(), tmp1));
                bdd.deref(tmp1);
                bdd.deref(r.getHit());
                r.setHit(tmp2);
            }
            if (!bddused) {
                bdd.deref(tmp);
            }
            bddused = false;
        }
        device.addRule(rule);
        return changes;
    }

    public LinkedList<Device> addRuleAndVerifyInvariants(Device device, Rule rule) {
//        ArrayList<Long> track = new ArrayList<>();
//        TimeTracker timeTracker = TimeTracker.getInstance();
//        long start = System.nanoTime();

        HashSet<Integer> transferredPreds = this.addRule(device, rule);
        DeltaForwardingGraph dfg = new DeltaForwardingGraph(transferredPreds, this.model);
        Verifier verifier = new Verifier(dfg, new HashSet<>());
        return verifier.checkInvariants();
//        long end = System.nanoTime();
//        track.add(start);
//        track.add(end);
//        track.add((long) result);
//        timeTracker.addTrack(track);
    }
}
